import java.io.BufferedReader;
import java.io.IOException;
import java.io.InputStreamReader;
import java.util.ArrayList;
import java.util.Collections;
import java.util.Comparator;

public class ClauseForm {

	static String expression;
	static ArrayList<Character> variables = new ArrayList<Character>();
	static boolean traceMode = false; //flag for trace mode

	/**
	 * @param args
	 * 
	 * takes the FOL expression from the user and save it in the class
	 * variable expression which will be translated to CNF then to clause 
	 * form and also takes the mode type he want to use (either trace mode
	 * of regular mode).
	 */
	public static void main(String[] args) {
		try {
			BufferedReader reader = new BufferedReader(new InputStreamReader(System.in));
		
			// printing instructions
			System.out.println("ClauseForm Instructions: \n 1) Universal Quantifier: forAll" +
					"\n 2) Existential Quantifier: thereExist \n 3) Quantifier variables in braces: " +
					"forAll{x}, thereExist{x,y} \n 4) Expressions in square brackets: [P(x) v Q(y)] \n " +
					"5) Function Variables in parenthesis: P(x), Q(x,y) \n 6) Equivalence: <-> \n 7) Implication: ->" +
					" \n 8) Conjunction: ^ \n 9) Disjunction: v \n 10) Negation: ~ \n\n A valid expression can be the" +
					" following: forAll{x}[P(x)<->[Q(x)^thereExist{y}[Q(y)^R(y,x)]]] \n");
			
			System.out.println("Enter the FOL expression:");
			
			expression = reader.readLine().trim();
			expression = expression.replaceAll(" ", "");
			
			System.out.println("For regular mode enter 'r', For trace mode enter 't':");
			
			String mode = reader.readLine().trim(); // mode type input
			mode = mode.replaceAll(" ", "");
			
			if(mode.equalsIgnoreCase("t")) 
				traceMode = true;
			else if(mode.equalsIgnoreCase("r")) 
				traceMode = false;
			
			while(!mode.equalsIgnoreCase("t") && !mode.equalsIgnoreCase("r")){
			
				System.out.println("For regular mode enter 'r', For trace mode enter 't':");
				
				mode = reader.readLine().trim(); // mode type input
				mode = mode.replaceAll(" ", "");
				
				if(mode.equalsIgnoreCase("t")) 
					traceMode = true;
				else if(mode.equalsIgnoreCase("r")) 
					traceMode = false;
			}
			
			reader.close();
			
			//expression = "forAll{x}[P(x)<->[Q(x)^thereExist{y}[Q(y)^R(y,x)]]]";
			//expression = "thereExist{x}[P(x)^forAll{x}[Q(x)->~P(x)]]";
			
			System.out.println("Original Expression: " + expression);
			System.out.println();
			
			if((listOfOccurances('[', expression).size() != listOfOccurances(']', expression).size()) || 
					(listOfOccurances('(', expression).size() != listOfOccurances(')', expression).size()) || 
					(listOfOccurances('{', expression).size() != listOfOccurances('}', expression).size()))
				System.out.println("Invalid bracketing");
			
			else{
				convertToCNF();
				convertToClauseForm();
			}
			
		} catch (IOException e) {
			e.printStackTrace();
		}

	}
	
	
	/**
	 * this method calls all the steps of the converting of FOL
	 * expression to CNF and prints the final CNF
	 */
	public static void convertToCNF(){
		
		try{
			eliminateEquivalance();
			eliminateImplication();
			pushNegation();
			standardizeApart();
			skolemize();
			discardForAll();
			translateIntoCNF();
			flattenBrackets();
		
			System.out.println("Final Expression in CNF: " + expression);
			System.out.println();
		}
		catch(Exception e){
			System.out.println("Wrong expression format");
		}
	}
	
	
	/**
	 * This method calls all the steps to convert from CNF to clause form
	 * and prints the final generated clause form 
	 */
	public static void convertToClauseForm(){
		
		try{
			transformToClauses();
			standardizeApartClauseForm();
		
			System.out.println("Final Expression in ClauseForm: " + expression);
			System.out.println();
		}
		catch(Exception e){
			System.out.println("Wrong expression format");
	}
		
	}
	
	
	/**
	 * This method eliminates the equivalence by searching for
	 * all equivalence signs and applying the rule of replacing 
	 * each equivalence with 2 implications.
	 */
	public static void eliminateEquivalance(){
		
		ArrayList<Integer> occurances = listOfOccurances('<', expression); //getting all occurrences of equivalence
		
		for(int i = 0; i < occurances.size(); i++){
			
			int occurance = expression.indexOf('<'); 
			ArrayList<Integer> scope = getScope(occurance); // getting the scope that this occurrence of equivalence affect 
			String leftExp = expression.substring(scope.get(0)+1, occurance); // getting the left part of expression (before equivalence)
			String rightExp = expression.substring(occurance+3, scope.get(1)); // getting the right part of expression (after equivalence)
			
			expression = expression.replace(expression.substring(scope.get(0)+1, scope.get(1)), 
					"[" + leftExp + "->" + rightExp + "]^[" + rightExp + "->" + leftExp + "]"); //replacing the scope of equivalence with two implications
		}
		if(traceMode){ //if in trace mode prints tracing steps
			System.out.println("Eliminate Equivalance: " + expression);
			System.out.println();
		}
	}
	
	/**
	 * This method eliminates the implication by searching for
	 * all implication signs and applying the rule of replacing 
	 * each implication.
	 */
	public static void eliminateImplication(){
		
		ArrayList<Integer> occurances = listOfOccurances('>', expression); //getting all occurrences of implication
		
		for(int i = 0; i < occurances.size(); i++){
			
			int occurance = expression.indexOf('>');
			ArrayList<Integer> scope = getScope(occurance);//getting the scope that this implication affect 
			String leftExp = expression.substring(scope.get(0)+1, occurance-1); //getting the left part of expression (before implication) 
			String rightExp = expression.substring(occurance+1, scope.get(1)); //getting the right part of expression (after implication) 
			
			expression = expression.replace(expression.substring(scope.get(0)+1, scope.get(1)), 
					"~" + leftExp + "v" + rightExp + ""); //replacing the scope of implication with not and or
			
		}
		if(traceMode){ //if in trace mode prints tracing steps
			System.out.println("Eliminate Implication: " + expression);
			System.out.println();
		}
	}
	
	
	/**
	 * In this method negation sign is pushed into the brackets by applying
	 * all the rules of pushing the negation first by searching and replacing 
	 * all extra negations with the appropriate replacement then for each negation
	 * outside a bracket it is pushed and all the elements in the bracket are negated
	 */
	public static void pushNegation(){
		
		while(expression.contains("~[") || expression.contains("~~") 
				||expression.contains("~forAll") || expression.contains("~thereExist")){ //looping until all negations required to be pushed doesn't exist
			
			expression = expression.replaceAll("~~", ""); //removing all double negations
			expression = expression.replaceAll("~forAll", "thereExist"); //replacing the negation of forAll with thereExisit
			expression = expression.replaceAll("~thereExist", "forAll"); //replacing the negation of thereExist with forAll
			
			int occurance = expression.indexOf("~["); // getting the first occurrence of negation that need to be pushed in a bracket
			
			if(expression.contains("~[")){ 
				ArrayList<Integer> scope = getRightScope(occurance); //Getting the scope that this negation affect
				String tempString = expression.substring(occurance, scope.get(1)); //taking the scope in a string
				
				if(tempString.contains("^")){ 
					tempString = tempString.substring(1);
					
					for(int i =0; i < tempString.length(); i++){
						//changing all the elements with there corresponding change 
						if(tempString.charAt(i) == '[') 
							tempString = tempString.substring(0, i) + "[~" + tempString.substring(i+1, tempString.length());
						else if(tempString.charAt(i) == '^')
							tempString = tempString.substring(0, i) + "v~" + tempString.substring(i+1, tempString.length());
						else if(tempString.charAt(i) == 'v')
							tempString = tempString.substring(0, i) + "^~" + tempString.substring(i+1, tempString.length());
					}
				}
			
			expression = expression.replace(expression.substring(occurance, scope.get(1)),tempString);//replacing the scope with changes done
			}
		}
		if(traceMode){ //if in trace mode prints tracing steps
			System.out.println("Push Negation: " + expression);
			System.out.println();
		}
	}
	
	
	/**
	 * This method checks and replaces any variable that is repeated in more than
	 * one quantifier first by searching for all the quantifiers and getting their
	 * elements then checking one quantifier after the other if there are elements 
	 * repeated or not, if there are elements are replaced with new ones
	 */
	public static void standardizeApart(){
		
		ArrayList<Integer> occurances = listOfStringOccurances("forAll", expression); //getting all occurreance of forall
		occurances.addAll(listOfStringOccurances("thereExist", expression)); //getting all occurrences of thereexist
		occurances = sortListAsc(occurances); //sorting list ascendingly to sort the occurrences of both quantifiers in the expression
		
		for(int i = 0; i < occurances.size(); i++){
			int occurance = occurances.get(i);
			ArrayList<Character> elements = getQuantifiersElements(occurance); //getting all elements of each quantifier
			ArrayList<Integer> scope = getRightScope(occurance); // getting the scope that is affected by this quantifier

			for(int j = 0; j < elements.size(); j++){
				
				if(variables.contains(elements.get(j))){ //checking if element appeared before in another quantifier
					String tempString = expression.substring(scope.get(0)-3, scope.get(1)); 
					
					char c = 'a'; 
					while(variables.contains(c)) c++; //getting a char that was not used before
					tempString = tempString.replace(elements.get(j), c); //replacing every occurrence of this element with the new char
					
					expression = expression.replace(expression.substring(scope.get(0)-3, scope.get(1)),
							tempString);
					variables.add(c); //adding char to the list of already occurred elements
				}else
					variables.add(elements.get(j)); //adding this element to the list of variables
			}
		}
		if(traceMode){ //if in trace mode prints tracing steps
			System.out.println("Standardize Apart: " + expression);
			System.out.println();
		}
		
	}
	
	
	/**
	 * This function removes all existential quantifiers gets the 
	 * scope of quantifier and replaces each of its variables with 
	 * a function (with a name that is not used before) of the
	 * variables of the universal quantifier
	 */
	public static void skolemize(){
		
		ArrayList<Integer> occurances = listOfStringOccurances("forAll", expression); //getting all occurences of forall
		occurances = sortListDesc(occurances); //sorting descending to loop from inside out 
		
		for(int i = 0; i < occurances.size(); i++){ 
			int occurance = occurances.get(i);
			ArrayList<Character> elements = getQuantifiersElements(occurance); //getting all elements of this quantifier
			ArrayList<Integer> scope = getRightScope(occurance); //getting the scope that this quantifier affect
		
			while(expression.substring(scope.get(0), scope.get(1)).contains("thereExist")){ //looping until all thereexist in this scope are removed
				
				int occurance2 = expression.substring(scope.get(0), scope.get(1)).indexOf("thereExist")+scope.get(0); //getting the scope of the first occurance of thereexist
				ArrayList<Character> elements2 = getQuantifiersElements(occurance2); //getting all elements of this quantifier
				ArrayList<Integer> scope2 = getRightScope(occurance2); //getting the scope of this quantifier
				
				for(int j = 0; j < elements2.size(); j++){ //looping on elements of thereexist
					
					String thereExistString = expression.substring(scope2.get(0), scope2.get(1));
					char f = 'A';
					while(getFunctionList().contains(f)) f++; // getting a new function name that was not used
					thereExistString = thereExistString.replaceAll(elements2.get(j).toString(), 
							(f+"("+ elements.toString().substring(1, elements.toString().length()-1)+")")); //replacing all elements with function name
					
					expression = expression.replace(expression.substring(scope2.get(0)-13, scope2.get(1)),
							thereExistString); //repacing this scope in the expression with the edited string
					scope = getRightScope(occurance); 
				
				}
			}
			
		}
		while(expression.contains("thereExist")){ //looping until all there exist are removed this is used if thereexist occurs not in the scope of forall
			expression = expression.substring(0,expression.indexOf("thereExist")) + 
				expression.substring(expression.indexOf("}")+1,expression.length());//removing thereexist and all its elements
		}
		if(traceMode){ //if in trace mode prints tracing steps
			System.out.println("Skolemize: " + expression);
			System.out.println();}
	}
	
	
	/**
	 * discards all the forAll in the expression
	 */
	public static void discardForAll(){
		
		while(expression.contains("forAll")){ //looping until all forAll are removed
		
			expression = expression.substring(0,expression.indexOf("forAll")) + 
					expression.substring(expression.indexOf("}")+1,expression.length()); //removing forall and all its elements
		
		}
		if(traceMode){ //if in trace mode prints tracing steps
			System.out.println("Discard ForAll: " + expression);
			System.out.println();
		}
	}

	/**
	 * calls the methods of translating to CNF then prints the CNF translated
	 * expression
	 */
	public static void translateIntoCNF(){
		
		translateIntoCNF1();
		translateIntoCNF2();
		
		if(traceMode){ //if in trace mode prints tracing steps
			System.out.println("Translate to CNF: " + expression);
			System.out.println();
		}
	}
	
	/**
	 * finds all 'and' signs that need to be pushed in a bracket, 
	 * and change the expression with the corresponding correct change.
	 */
	public static void translateIntoCNF1(){
		
		int changeInSize = 0; //used to merging between edited expression and the real one
		ArrayList<Integer> occurances = listOfOccurances('^', expression); //getting all and occurrences in the expression
		
		for(int i = 0; i < occurances.size(); i++){
			changeInSize = 0; 
			int occurance = expression.indexOf("^["); //getting first occurrence of and that need to be pushed into a bracket
			
			if(occurance != -1 && expression.charAt(occurance-1) != ']'){ 
				ArrayList<Integer> scope = getScope(occurance); //getting the scope of this occurrence 
				String leftExp = expression.substring(scope.get(0)+1, occurance); //getting the left part of the scope (before the and)
			
				ArrayList<Integer> occurances2 = getOperatorOcurrances('v', occurance+1 ,scope.get(1)); //get all occurrences of or in this scope
				
				for(int j = 0; j < occurances2.size(); j++){ //looping on or occurrences
					
					int orOccurance = occurances2.get(j) + changeInSize; //merging the edited string with the real one
					ArrayList<Integer> scope2 = getScope(orOccurance); //getting the scope that this occurrence affect
					String orleftExp = expression.substring(scope2.get(0)+1, orOccurance); //getting the left of or part
					String orrightExp = expression.substring(orOccurance+1, scope2.get(1)); //getting the right of or part
					
					changeInSize = ("[" + leftExp + "^" + orleftExp + "]v[" + leftExp + "^" + orrightExp + "]").length()
						-expression.substring(scope.get(0)+1, scope.get(1)).length(); //calculating the amount of change in size between the old and the edited ones
					
					expression = expression.replace(expression.substring(scope.get(0)+1, scope.get(1)), 
							"[" + leftExp + "^" + orleftExp + "]v[" + leftExp + "^" + orrightExp + "]");//replacing with the edited string
				}
			}
		}
	}
	
	
	/**
	 * finds all 'or' signs that need to be pushed in a bracket, 
	 * and change the expression with the corresponding correct change.
	 */
	public static void translateIntoCNF2(){
		
		int changeInSize = 0;  //used to merge between edited expression and the real one
		int changed = 0; 
		
		while((expression.contains("v[") || expression.contains("]v")) && changed >= 0){ //looping until all ands that needs to be pushed in brackets are pushed
			int temp = 0;
			
			changeInSize = 0;
			int occurance = expression.indexOf("v["); //getting the first occurrence of and that need to be pushed
			
			if(occurance == -1) {
				occurance = expression.indexOf("]v"); 
				temp = 1;
			}
			
			if(occurance != -1){
				ArrayList<Integer> scope = getScope(occurance+temp); //getting the scope that will be affected by pushing this or
	
				changed--;
					

				String leftExp = expression.substring(scope.get(0)+1, occurance+temp);//getting the left of or part
				String rightExp = expression.substring(occurance+1+temp, scope.get(1));//getting the right of or part
				ArrayList<Integer> occurances2 = getOperatorOcurrances('^', occurance+1, scope.get(1));//getting all and occurrences in the right part
				if(occurances2.size() > 0){//if there exist and in the right hand expression
				
					for(int j = 0; j < occurances2.size(); j++){ //loops on and occurrences
					
						int andOccurance = occurances2.get(j)+changeInSize;  
						ArrayList<Integer> scope2 = getScope(andOccurance); //getting the scope that is affected by this and
						String andleftExp = expression.substring(scope2.get(0)+1, andOccurance); //getting left of and part
						String andrightExp = expression.substring(andOccurance+1, scope2.get(1)); //getting right of and part
					
						changeInSize = ("[" + leftExp + "v" + andleftExp + "]^[" + leftExp + "v" + andrightExp + "]").length()
								-expression.substring(scope.get(0)+1, scope.get(1)).length(); //calculating the change in size
						changed = 1;
						expression = expression.replace(expression.substring(scope.get(0)+1, scope.get(1)), 
								"[" + leftExp + "v" + andleftExp + "]^[" + leftExp + "v" + andrightExp + "]"); 
					}
				}
				else {

					occurances2 = getOperatorOcurrances('^', scope.get(0)+1, occurance); //getting all and occurrences in the left part

					changeInSize = 0;
				
					for(int j = 0; j < occurances2.size(); j++){
						
						int andOccurance = occurances2.get(j)+changeInSize;
						ArrayList<Integer> scope2 = getScope(andOccurance); //getting all and occurrences in the right part
						String andleftExp = expression.substring(scope2.get(0)+1, andOccurance); //getting left of and part
						String andrightExp = expression.substring(andOccurance+1, scope2.get(1)); //getting right of and part
						
						changeInSize = ("[" + leftExp + "v" + andleftExp + "]^[" + leftExp + "v" + andrightExp + "]").length()
						-expression.substring(scope.get(0)+1, scope.get(1)).length(); //calculating the change in size
						
						changed = 1;
						
						expression = expression.replace(expression.substring(scope.get(0)+1, scope.get(1)), 
								"[" + andleftExp + "v" + rightExp + "]^[" + andrightExp + "v" + rightExp + "]");
					}
				}
			}
		}
	}
	
	/**
	 * This method removes any redundant brackets in the expression
	 */
	public static void flattenBrackets(){
		
		while(expression.contains("[[") || expression.contains("]]") || 
								expression.contains("]v") || expression.contains("v[")){
			
			expression = expression.replaceAll("\\[\\[", "[");
			expression = expression.replaceAll("\\]\\]", "]");
			expression = expression.replaceAll("v\\[", "v");
			expression = expression.replaceAll("\\]v", "v");
		}
		
		expression = "[" + expression + "]";
		
		if(traceMode){ //if in trace mode prints tracing steps
		System.out.println("Flatten Brackets: " + expression);
		System.out.println();
		}
	}
	
	/**
	 * This method transforms the expression to clause form by replacing each square bracket
	 * with a brace and each and or or with a comma
	 */
	public static void transformToClauses(){
		
		expression = expression.replaceAll("\\[", "{");
		expression = expression.replaceAll("\\]", "}");
		expression = expression.replaceAll("v", ",");
		expression = expression.replaceAll("\\^", ",");
		
		if(traceMode){ //if in trace mode prints tracing steps
			System.out.println("Transform to Clauses: " + expression);
			System.out.println();
		}
		
	}
	
	/**
	 * This method checks and replaces any variable that is repeated in more than
	 * one clause, first by dividing the expression into clauses and getting the
	 * variables of each clause then checking one clause after the other if there are elements 
	 * repeated or not, if there are elements are replaced with new ones
	 */
	public static void standardizeApartClauseForm(){
		
		ArrayList<String> clauses = getClauses(); //list of clauses
		ArrayList<String> clauseVariables = new ArrayList<String>(); //list of variables of each clause
		ArrayList<String> allVariables = new ArrayList<String>(); // list of all clauses variables
		String clause;
		boolean found;
		
		for(int i = 0 ; i < clauses.size() ; i++){
			
			clause = clauses.get(i);
			clauseVariables = getClauseVariables(clause); //get the variables of this clause
			
			for(int j = 0 ; j < clauseVariables.size() ; j++){
					
				found = false;
				String var1 = clauseVariables.get(j);
				String var2;
					
				for(int k = 0 ; k < allVariables.size() ; k++){
					
					var2 = allVariables.get(k);
					
					if(var2.equals(var1)){ //if clause variable is found in the list of all variables
						clause = clause.replaceAll(var1, var1+(i+1)); //replace the occurrences of var with var+(i+1)
						found = true;
						break;
					}
				}	
				if(!found) //if clause variable is not found in the list of all variables
					allVariables.add(var1);	//add variable to list of variables 
			}
			
			clause = "{" + clause + "}";
			clauses.set(i, clause); //put the changed clause in its position in the list of clauses 
		}
		
		expression = "{";
		for(int i = 0 ; i < clauses.size()-1 ; i++) //forming back the expression by concatenation the clauses 
			expression += clauses.get(i) + ", ";
		
		expression += clauses.get(clauses.size()-1)+"}";
		
		if(traceMode){ //if in trace mode prints tracing steps
			System.out.println("Standardize Apart ClauseForm: " + expression);
			System.out.println();
		}
	}
	
	/**
	 * This method gets the list of clauses in the expression
	 */
	public static ArrayList<String> getClauses(){
		
		ArrayList<String> clauses = new ArrayList<String>();
		String clause = "";
		boolean start = false;
		char c;
		for(int i = 1 ; i < expression.length()-1 ; i++){
			
			c = expression.charAt(i);
			
			if(c == '{')
				start = true;
			
			else if(c == '}'){
				start = false;
				clauses.add(clause);
				clause = "";
			}
			
			else if(start)
				clause += c;
			
		}
		
		return clauses;
	}
	
	/**
	 * This method gets the list of variable for the given clause
	 */
	public static ArrayList<String> getClauseVariables(String clause){
		
		ArrayList<String> clauseVariables = new ArrayList<String>();
		
		char c;
		boolean start = false;
		
		for(int i = 0 ; i < clause.length() ; i++){
			
			c = clause.charAt(i);
			
			if(c == '(')
				start = true;
			
			else if(c == ')')
				start = false;
			
			else if(start && c != ',' && !Character.isUpperCase(c)){
				
				boolean exist = false;
				
				for(int j = 0 ; j < clauseVariables.size() ; j++){
					if(clauseVariables.get(j).equals(c+"")){
						exist = true;
						break;
					}
				}
				if(!exist)
					clauseVariables.add(c+"");
			}
				
		}

		return clauseVariables;
	}
	
	/**
	 * This method takes a char 'c' and a string and return the list of positions where c occurred in the string
	 */
	private static ArrayList<Integer> listOfOccurances(char c, String term) {
		
		ArrayList<Integer> occurances = new ArrayList<Integer>();
		
		for(int i = 0 ; i < term.length() ; i++){
			
			if(term.charAt(i) == c)
				occurances.add(i);
		}
		
		return occurances;
	}
	
	/**
	 * This method takes a string 's' and a string and return the list of positions where s occurred in the string
	 */
	private static ArrayList<Integer> listOfStringOccurances(String s, String term) {
		
		ArrayList<Integer> occurances = new ArrayList<Integer>();
		
		while(term.contains(s)){
				occurances.add(term.indexOf(s));
				term = term.substring(term.indexOf(s)+s.length());		
		}
		return occurances;
	}
	
	/**
	 * This method takes a operator 'c', a starting index and an ending index, 
	 * and returns the list of positions where c occurred between the start and the end 
	 */
	public static ArrayList<Integer> getOperatorOcurrances(char c, int occurance, int end){

		ArrayList<Integer> occurances = new ArrayList<Integer>();
		int count = 0;
		for(int i = occurance; i < end; i++){
			if(expression.charAt(i) == '[')
				count++;
			else if(expression.charAt(i) == ']')
				count--;
			else if(expression.charAt(i) == c && count == 1)
				occurances.add(i);	
		}
		return occurances;
	}
	
	/**
	 * This method takes a quantifier position, and returns the list of elements of this quantifier 
	 */
	private static ArrayList<Character> getQuantifiersElements(int occurance) {
		ArrayList<Character> elements = new ArrayList<Character>();
		boolean start = false;
		for(int i = occurance; i < expression.length(); i++){
			if(expression.charAt(i) == '{')
				start = true;
			else if(expression.charAt(i) == '}'){
				start = false;
				break;
			}
			else if(expression.charAt(i) == ',')
				continue;
			else if(start)
				elements.add(expression.charAt(i));
		}
		return elements;
	}
	
	/**
	 * This method takes a list of integers and sorts it ascendingly  
	 */
	@SuppressWarnings("unchecked")
	public static ArrayList<Integer> sortListAsc(ArrayList<Integer> list){
		Collections.sort(list, new Comparator(){ 
			public int compare(Object o1, Object o2) {

			Integer first = (Integer) o1;
			Integer second = (Integer) o2;

			if(first.intValue() > second.intValue()) 
				return 1;
			else if(first.intValue() < second.intValue()) 
				return -1;

			return 0; 
			} 
		});
		return list;
	}
	
	/**
	 * This method takes a list of integers and sorts it descendingly  
	 */
	@SuppressWarnings("unchecked")
	public static ArrayList<Integer> sortListDesc(ArrayList<Integer> list){
		Collections.sort(list, new Comparator(){ 
			public int compare(Object o1, Object o2) {

			Integer first = (Integer) o1;
			Integer second = (Integer) o2;

			if(first.intValue() > second.intValue()) 
				return -1;
			else if(first.intValue() < second.intValue()) 
				return 1;

			return 0; 
			} 
		});
		return list;
	}

	/**
	 * This method returns a list of all functions in the expression, this is used in the skolemize step inorder
	 * to choose a function that is not used before
	 */
	private static ArrayList<Character> getFunctionList(){
		
		ArrayList<Character> functions = new ArrayList<Character>();
		
		for(int i = 1 ; i < expression.length() ; i++){
			
			if(expression.charAt(i) == '(')
				functions.add(expression.charAt(i-1));
		}
		
		return functions;
	}
	
	/**
	 * This method takes an index of a negation operator or a quantifier and returns the start and the end 
	 * of its scope in the expression
	 */
	private static ArrayList<Integer> getRightScope(int occurance) {
		ArrayList<Integer> scope = new ArrayList<Integer>();
		int count = 0;
		for(int i = occurance; i < expression.length(); i++){
			if(expression.charAt(i) == '['){
				if(count == 0){ //if this bracket is the first occurrence of [
					scope.add(i); //store start index
				}
				count++;
			}else if(expression.charAt(i) == ']'){
				count--;
				if(count == 0){ //if this is the end of the scope
					scope.add(i); //store end index
					break;
				}
			}
		}
		return scope;
	}
	
	/**
	 * This method takes an index of an operator (and, or, iff, imply) and returns the start and the end 
	 * of its scope in the expression
	 */
	private static ArrayList<Integer> getScope(int occurance) {
		ArrayList<Integer> scope = new ArrayList<Integer>();
		int count = 0;
		for(int i = occurance; i >= 0; i--){ //checking the part on the left of the operator
			if(expression.charAt(i) == '['){ 
				count--;
			}
			if(expression.charAt(i) == ']'){
				count++;
			}
			if(count < 0 || i == 0){ //if we hit a [ that has no corresponding ] or we reached the start of the expression
				scope.add(i); //store start index
				break;
			}
		}
		count = 0;
		for(int i = occurance; i < expression.length(); i++){ //checking the part on the right of the operator
			if(expression.charAt(i) == '['){ 
				count++;
			}
			if(expression.charAt(i) == ']'){
				count--;
			}
			if(count < 0 || i == expression.length()-1){ //if we hit a ] that has no corresponding [ or we reached the end of the expression
				scope.add(i); //store end index
				break;
			}
		}
		return scope;
	}

}
